Nuprl Definition : nondecreasing
4,23
postcript
pdf
nondecreasing(
f
;
k
) ==
i
:
(
k
-1).
f
(
i
)
f
(
i
+1)
latex
clarification:
nondecreasing(
f
;
k
) ==
i
:{0..(
k
-1)
}.
f
(
i
)
f
(
i
+1)
latex
Definitions
x
:
A
.
B
(
x
)
,
{
i
..
j
}
,
A
B
FDL editor aliases
nondecreasing
origin
i:
(k-1). f(i)
f(i+1)
i:{0..(k-1)
}. f(i)f(i+1) i:(k-1). f(i)f(i+1)
i:{0..(k-1)}. f(i)f(i+1) x:A. B(x)}B